$\forall$${\it es}$:ES, $L$:(E List), $e$:E, $i$:Id. \\[0ex]loc{-}on{-}path(${\it es}$;$i$;[$e$ / $L$]) $\Leftarrow\!\Rightarrow$ ((loc($e$) = $i$) $\vee$ loc{-}on{-}path(${\it es}$;$i$;$L$))